$\forall$$a$:Atom1, $A$:MsgA, $s$:$A$.state.
\\[0ex]AtomFree(ds($A$))
\\[0ex]$\Rightarrow$ AtomFree(da($A$))
\\[0ex]$\Rightarrow$ $\lambda$$x$.$A$.init($x$)?$s$($x$):$A$.state$>>$$a$
\\[0ex]$\Rightarrow$ ma{-}body($A$):Shape($A$)$>>$$a$ $\vee$ $s$:$A$.state$>>$$a$